We now introduce some background notions on Minsky machines, well-structured transition systems (WSTS), 
and Petri nets. 

\subsection{Minsky machines}
Our undecidability results will be obtained by encodings of \emph{Minsky machines} \cite{Minsky67}. 
A Minsky machine (\mm)  is a Turing complete 
model composed of a set of sequential, labeled   instructions, and two registers.   
Registers $r_j ~(j \in \{0,1\})$ can hold arbitrarily large natural numbers.   
Instructions $(1:I_1), \ldots, (n:I_n)$ can be of three kinds:  
$\mathtt{INC}(r_j)$ adds 1 to register $r_j$ and proceeds to the next instruction;  
$\mathtt{DECJ}(r_j,s)$ jumps to instruction $s$ if $r_j$ is zero, otherwise it decreases register $r_j$ by 1 and proceeds to the next instruction;
a $\mathtt{HALT}$ instruction stops the machine. 
A \mm includes a program counter $p$ indicating the label of the instruction  being executed.   

In its initial state, the machine has both registers set to $0$ and the program counter $p$ set to the first instruction.  
%that the machine starts with zero in both registers and that $(1:I_1)$ is the first instruction to be  
%executed.   
We assume that instructions are proper, in the sense that there is no program counter that refers to a non-existing instruction.
The \mm \emph{terminates} whenever the program counter is set to a $\mathtt{HALT}$ instruction.
%
%i.e., when $p > n$;
%for convenience, we make the 
%unrestrictive assumption that the machine stops  
%when the program counter is set to a special new
%instruction $\mathtt{HALT}$.
A \emph{configuration} of a \mm is a tuple $(i,m_0,m_1)$; it consists of the current program counter and the values of the registers. Formally, the reduction relation  
over configurations of a \mm, denoted $\minskred$, is defined 
in Figure \ref{a:mm}.
%in Appendix \ref{a:mm}.
%Minsky machines are Turing complete \cite[Chapter 14]{Minsky67}.

Since \mmss are Turing complete, termination is undecidable.

\begin{theorem}[Minsky
%\cite[Theorem 14.1-1]
\cite{Minsky67}]
Minsky machines are Turing complete.
Hence, for a \mm it is undecidable whether it terminates.
\qed
\end{theorem}

We shall exploit encodings into \mmss to prove undecidability of \LG and \OG. %bounded and eventual adaptation.
In our encodings, we sometimes make the unrestrictive assumption that 
at the beginning and at the end of the computation the
registers (must) contain the value zero.

 \begin{figure}[t]
  \linefigure
  \begin{mathpar}  
 \inferrule[\textsc{(M-Inc)}]{i:\mathtt{INC}(r_j) \ \ m_j' = m_j + 1 \ \ m_{1-j}' = m_{1-j}}{(i,m_0,m_1)\minskred(i+1,m_0',m_1')}  
 \quad 
 \inferrule[\textsc{(M-Jmp)}]{i:\mathtt{DECJ}(r_j,s) \quad m_j = 0}{(i,m_0,m_1)\minskred(s,m_0,m_1)}  
 \and  
 \inferrule[\textsc{(M-Dec)}]{i:\mathtt{DECJ}(r_j,s) \quad m_j \neq 0 \quad  m_j' = m_j - 1 \quad m_{1-j}' = m_{1-j}}{(i,m_0,m_1)\minskred(i+1,m_0',m_1')}
 \end{mathpar}  
 \caption{Semantics of \mmss}\label{a:mm}
  \linefigure
\end{figure}

\subsection{Well-Structured Transition Systems}\label{s:wsts}
The decidability of \OG for \evold{2} processes will be shown by appealing to the theory of
well-structured transition systems \cite{FinkelS01,AbdullaCJT00}.
The following results and definitions are from \cite{FinkelS01},  unless
differently specified. 

\input{finkel}

\subsection{Petri Nets}\label{sec:petri}
We will use Petri nets to prove the decidability of \OG for \evols{3}. 
More precisely,
we will reduce \OG  for \evols{3} to a problem on Petri nets, that we call
\emph{infinite visit}, which can be easily reduced to place boundedness.

A \emph{Petri net}  %(see e.g. \cite{EN94})
is a tuple $N = (S, T, m_0 )$, where $S$ and $T$
are finite sets of \emph{places} and \emph{transitions}, respectively.
A finite multiset over the set $S$ of places is called a \emph{marking}, and $m_0$ is the initial marking.
Given a marking $m$ and a place $p$, we say that the place $p$
contains $m(p)$ \emph{tokens} in the marking $m$ if there are $m(p)$ occurrences of $p$ in the multiset $m$.
A transition is a pair of markings
written in the form $m'\derriv{}m''$.
The marking $m$ of a Petri net can be modified
by means of transition firing: a transition
$m'\derriv{}m''$ can fire if
$m(p) \geq m'(p)$ for every place $p \in S$;
upon transition firing the
new marking of the net becomes $n=(m \setminus m') \uplus m''$
where $\setminus$ and $\uplus$ are the difference and
union operators for multisets, respectively.
This is written as $m \derivv n$.
We call \emph{computation} a sequence $m_{0}\derivv m_{1}\derivv \cdots \derivv m_{n}$.
A marking $m$ is \emph{reachable} if there exists 
a computation with final marking $m$.
A place $p \in S$ is \emph{bounded}
if there exists a natural number $k$ such that $m(p) \leq k$
for every reachable marking $m$.
The place boundedness problem is decidable for Petri nets~\cite{KarpM69}.

\begin{definition}[Infinite visit]\label{d:infvisit}
Given a Petri net $N = (S, T, m_0)$, a 
set of places to visit $V \subseteq S$, 
and a mandatory place $p \in S$,
we say that $N$
\emph{infinitely visits} $V$ with mandatory place $p$,
if there exists an infinite sequence 
$m_{0}\derivv m_{1}\derivv m_{2} \derivv \cdots$ and an index $i$ such that for every $j \geq i$ there exists a place $p_j \in V$
such that $m_{j}(p_j) \geq 1$, and moreover $m_{j}(p) \geq 1$.
\end{definition}

\begin{theorem}\label{th:infiniteVisit}
Given a Petri net $N = (S, T, m_0)$, a 
set of places $V \subseteq S$, and a mandatory place $p \in S$,
it is decidable whether $N$
\emph{infinitely visits} $V$ with mandatory place $p$.
\end{theorem}
\begin{proof}
The proof is by reduction to the place boundedness
problem. Given a Petri net $N = (S, T, m_0)$
and a set of places $V \subseteq S$,
we construct a Petri net $N' = (S\cup \{ph1,ph2,check\}, T', m_0\cup\{ph1\})$
such that $N$ infinitely visits $V$ with mandatory place $p$
if and only if $check$
is not bounded in $N'$.

The Petri net $N'$ reproduces the computations
in $N$ by (possibly) dividing them into two phases:
the first phase is witnessed by the presence of one
token in the additional place $ph1$, while
the second phase by one token in the additional
place $ph2$. During the second phase, a transition
can be mimicked only if there is at least one token 
in one of the places in $V$ and one token in the place
$p$. Moreover, during the second
phase, each transition puts one token in the additional place $check$.

Formally, we define the set $T'$ of the transitions of $N'$ as follows:
\begin{itemize}
\item
for each transition $m' \derriv{} m''$ in $T$, $T'$ contains 
the transition $m'\uplus\{ph1\} \derriv{} m''\uplus\{ph1\}$;
\item
$T'$ contains the transition $\{ph1\} \derriv{} \{ph2\}$;
\item
for each transition $m' \derriv{} m''$ in $T$ and for each place 
$q \in V$, 
$T'$ contains the transition $m'\uplus\{p,q,ph2\} \derriv{} m''\uplus\{p,q,ph2,check\}$.
\end{itemize}
The first group of transitions governs the first phase of the
simulation; the second transition implies the passage from the
first to the second phase; while the third group of transitions
is for the second phase.

First, assume that $N$ infinitely visits $V$ with mandatory place $p$. 
This means that in $N$
there
exists an infinite sequence 
$m_{0}\derivv m_{1}\derivv m_{2} \derivv \cdots$ and an index $i$ such that for every $j \geq i$ there exists a place $p_j \in V$
such that $m_{j}(p_j) \geq 1$ and $m_{j}(p) \geq 1$.
This implies that in $N'$ there is a corresponding 
computation that mimics the transition $m_{0}\derivv m_{1}\derivv m_{2} \derivv m_{i-1}$ during the first phase,
and the transitions $m_{i}\derivv m_{i+1}\derivv \cdots$ 
during the second one. The second phase is infinite, hence $check$
is not bounded because each transition in the second phase
puts one token in such a place.

Assume now that $check$ is unbounded in $N'$.
As tokens are introduced in $check$ only during the second
phase, this means that there exists no bound
to the length of the computations in $N'$ that
include the second phase. This implies the existence of at least one infinite
computation in $N'$ having both the first and the second phase.
Consider now the computation in $N$ composed of the
transitions simulated in such an infinite computation of $N'$.
This computation in $N$ has a 
suffix (the part corresponding to the second phase)
in which all the traversed markings have
at least one token in one of the places in $V$
as well as one token in $p$. 
\end{proof}


 
%(which is known to be decidable~\cite{KarpM69}). 
%Namely, given a Petri net $N = (S, T, m_0 )$,
%a place $p \in S$ is \emph{bounded}
%if there exists a value $k$ such that $m(p) \leq k$
%for every marking $m$ reachable from $m_{0}$.



%verification of a property on Petri nets that we call
%\emph{infinite coverability}.
%\begin{definition}[Infinite coverability]
%Given a Petri net $N = (S, T, m_0)$ and two markings $m'$ and $m''$
%of $N$, we say that $m''$ \emph{covers} $m'$
%if $m'(p) \leq m''(p)$ for every place $p \in S$.
%We say that $N$ \emph{infinitely covers} the marking $m$ if there exists 
%an infinite sequence $m_{0}\derivv m_{1}\derivv m_{2} \derivv \cdots$ and an index $i$ such that $m_{j}$ covers $m$ for every $j \geq i$.
%\end{definition}




%A marking $m_{n}$ is \emph{reachable} if there exists 
%a sequence $m_{0}\derivv m_{1}\derivv \cdots \derivv m_{n}$.
%A marking $m$ is \emph{coverable} if there exists a marking $m'$ such that $m \subseteq m'$. By means of the coverability tree algorithm it has been showed that it is decidable whether a marking is coverable. 
%
%\begin{theorem}[Karp Miller \cite{KarpM69}]\label{teo:cov}
%The coverability problem is decidable for Petri Nets. 
%\end{theorem}


%A place $p$ is {\em bound} if there exists $k$ such that
%for each reachable marking $m$ we have that $m(p) \leq k$.
%It is well known that place boundedness  
%is decidable in Petri nets (this can be checked, e.g.,
%by verifying if all the markings in the coverability 
%tree~\cite{KarpM69} do not contain $\omega$ in the place 
%to be checked). 

%\subsection{The Spatial Logic \Lo}\label{ss:logic}
%   \input{logic}

%\subsection{Coverability}\label{ss:coverability}
%  \input{cover}